↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
average_in_gag(0, 0, 0) → average_out_gag(0, 0, 0)
average_in_gag(0, s(0), 0) → average_out_gag(0, s(0), 0)
average_in_gag(0, s(s(0)), s(0)) → average_out_gag(0, s(s(0)), s(0))
average_in_gag(s(X), Y, Z) → U1_gag(X, Y, Z, average_in_agg(X, s(Y), Z))
average_in_agg(0, 0, 0) → average_out_agg(0, 0, 0)
average_in_agg(0, s(0), 0) → average_out_agg(0, s(0), 0)
average_in_agg(0, s(s(0)), s(0)) → average_out_agg(0, s(s(0)), s(0))
average_in_agg(s(X), Y, Z) → U1_agg(X, Y, Z, average_in_agg(X, s(Y), Z))
average_in_agg(X, s(s(s(Y))), s(Z)) → U2_agg(X, Y, Z, average_in_gaa(s(X), Y, Z))
average_in_gaa(0, 0, 0) → average_out_gaa(0, 0, 0)
average_in_gaa(0, s(0), 0) → average_out_gaa(0, s(0), 0)
average_in_gaa(0, s(s(0)), s(0)) → average_out_gaa(0, s(s(0)), s(0))
average_in_gaa(s(X), Y, Z) → U1_gaa(X, Y, Z, average_in_aga(X, s(Y), Z))
average_in_aga(0, 0, 0) → average_out_aga(0, 0, 0)
average_in_aga(0, s(0), 0) → average_out_aga(0, s(0), 0)
average_in_aga(0, s(s(0)), s(0)) → average_out_aga(0, s(s(0)), s(0))
average_in_aga(s(X), Y, Z) → U1_aga(X, Y, Z, average_in_aga(X, s(Y), Z))
average_in_aga(X, s(s(s(Y))), s(Z)) → U2_aga(X, Y, Z, average_in_gaa(s(X), Y, Z))
average_in_gaa(X, s(s(s(Y))), s(Z)) → U2_gaa(X, Y, Z, average_in_gaa(s(X), Y, Z))
U2_gaa(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_gaa(X, s(s(s(Y))), s(Z))
U2_aga(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_aga(X, s(s(s(Y))), s(Z))
U1_aga(X, Y, Z, average_out_aga(X, s(Y), Z)) → average_out_aga(s(X), Y, Z)
U1_gaa(X, Y, Z, average_out_aga(X, s(Y), Z)) → average_out_gaa(s(X), Y, Z)
U2_agg(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_agg(X, s(s(s(Y))), s(Z))
U1_agg(X, Y, Z, average_out_agg(X, s(Y), Z)) → average_out_agg(s(X), Y, Z)
U1_gag(X, Y, Z, average_out_agg(X, s(Y), Z)) → average_out_gag(s(X), Y, Z)
average_in_gag(X, s(s(s(Y))), s(Z)) → U2_gag(X, Y, Z, average_in_gaa(s(X), Y, Z))
U2_gag(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_gag(X, s(s(s(Y))), s(Z))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PrologToPiTRSProof
average_in_gag(0, 0, 0) → average_out_gag(0, 0, 0)
average_in_gag(0, s(0), 0) → average_out_gag(0, s(0), 0)
average_in_gag(0, s(s(0)), s(0)) → average_out_gag(0, s(s(0)), s(0))
average_in_gag(s(X), Y, Z) → U1_gag(X, Y, Z, average_in_agg(X, s(Y), Z))
average_in_agg(0, 0, 0) → average_out_agg(0, 0, 0)
average_in_agg(0, s(0), 0) → average_out_agg(0, s(0), 0)
average_in_agg(0, s(s(0)), s(0)) → average_out_agg(0, s(s(0)), s(0))
average_in_agg(s(X), Y, Z) → U1_agg(X, Y, Z, average_in_agg(X, s(Y), Z))
average_in_agg(X, s(s(s(Y))), s(Z)) → U2_agg(X, Y, Z, average_in_gaa(s(X), Y, Z))
average_in_gaa(0, 0, 0) → average_out_gaa(0, 0, 0)
average_in_gaa(0, s(0), 0) → average_out_gaa(0, s(0), 0)
average_in_gaa(0, s(s(0)), s(0)) → average_out_gaa(0, s(s(0)), s(0))
average_in_gaa(s(X), Y, Z) → U1_gaa(X, Y, Z, average_in_aga(X, s(Y), Z))
average_in_aga(0, 0, 0) → average_out_aga(0, 0, 0)
average_in_aga(0, s(0), 0) → average_out_aga(0, s(0), 0)
average_in_aga(0, s(s(0)), s(0)) → average_out_aga(0, s(s(0)), s(0))
average_in_aga(s(X), Y, Z) → U1_aga(X, Y, Z, average_in_aga(X, s(Y), Z))
average_in_aga(X, s(s(s(Y))), s(Z)) → U2_aga(X, Y, Z, average_in_gaa(s(X), Y, Z))
average_in_gaa(X, s(s(s(Y))), s(Z)) → U2_gaa(X, Y, Z, average_in_gaa(s(X), Y, Z))
U2_gaa(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_gaa(X, s(s(s(Y))), s(Z))
U2_aga(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_aga(X, s(s(s(Y))), s(Z))
U1_aga(X, Y, Z, average_out_aga(X, s(Y), Z)) → average_out_aga(s(X), Y, Z)
U1_gaa(X, Y, Z, average_out_aga(X, s(Y), Z)) → average_out_gaa(s(X), Y, Z)
U2_agg(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_agg(X, s(s(s(Y))), s(Z))
U1_agg(X, Y, Z, average_out_agg(X, s(Y), Z)) → average_out_agg(s(X), Y, Z)
U1_gag(X, Y, Z, average_out_agg(X, s(Y), Z)) → average_out_gag(s(X), Y, Z)
average_in_gag(X, s(s(s(Y))), s(Z)) → U2_gag(X, Y, Z, average_in_gaa(s(X), Y, Z))
U2_gag(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_gag(X, s(s(s(Y))), s(Z))
AVERAGE_IN_GAG(s(X), Y, Z) → U1_GAG(X, Y, Z, average_in_agg(X, s(Y), Z))
AVERAGE_IN_GAG(s(X), Y, Z) → AVERAGE_IN_AGG(X, s(Y), Z)
AVERAGE_IN_AGG(s(X), Y, Z) → U1_AGG(X, Y, Z, average_in_agg(X, s(Y), Z))
AVERAGE_IN_AGG(s(X), Y, Z) → AVERAGE_IN_AGG(X, s(Y), Z)
AVERAGE_IN_AGG(X, s(s(s(Y))), s(Z)) → U2_AGG(X, Y, Z, average_in_gaa(s(X), Y, Z))
AVERAGE_IN_AGG(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GAA(s(X), Y, Z)
AVERAGE_IN_GAA(s(X), Y, Z) → U1_GAA(X, Y, Z, average_in_aga(X, s(Y), Z))
AVERAGE_IN_GAA(s(X), Y, Z) → AVERAGE_IN_AGA(X, s(Y), Z)
AVERAGE_IN_AGA(s(X), Y, Z) → U1_AGA(X, Y, Z, average_in_aga(X, s(Y), Z))
AVERAGE_IN_AGA(s(X), Y, Z) → AVERAGE_IN_AGA(X, s(Y), Z)
AVERAGE_IN_AGA(X, s(s(s(Y))), s(Z)) → U2_AGA(X, Y, Z, average_in_gaa(s(X), Y, Z))
AVERAGE_IN_AGA(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GAA(s(X), Y, Z)
AVERAGE_IN_GAA(X, s(s(s(Y))), s(Z)) → U2_GAA(X, Y, Z, average_in_gaa(s(X), Y, Z))
AVERAGE_IN_GAA(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GAA(s(X), Y, Z)
AVERAGE_IN_GAG(X, s(s(s(Y))), s(Z)) → U2_GAG(X, Y, Z, average_in_gaa(s(X), Y, Z))
AVERAGE_IN_GAG(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GAA(s(X), Y, Z)
average_in_gag(0, 0, 0) → average_out_gag(0, 0, 0)
average_in_gag(0, s(0), 0) → average_out_gag(0, s(0), 0)
average_in_gag(0, s(s(0)), s(0)) → average_out_gag(0, s(s(0)), s(0))
average_in_gag(s(X), Y, Z) → U1_gag(X, Y, Z, average_in_agg(X, s(Y), Z))
average_in_agg(0, 0, 0) → average_out_agg(0, 0, 0)
average_in_agg(0, s(0), 0) → average_out_agg(0, s(0), 0)
average_in_agg(0, s(s(0)), s(0)) → average_out_agg(0, s(s(0)), s(0))
average_in_agg(s(X), Y, Z) → U1_agg(X, Y, Z, average_in_agg(X, s(Y), Z))
average_in_agg(X, s(s(s(Y))), s(Z)) → U2_agg(X, Y, Z, average_in_gaa(s(X), Y, Z))
average_in_gaa(0, 0, 0) → average_out_gaa(0, 0, 0)
average_in_gaa(0, s(0), 0) → average_out_gaa(0, s(0), 0)
average_in_gaa(0, s(s(0)), s(0)) → average_out_gaa(0, s(s(0)), s(0))
average_in_gaa(s(X), Y, Z) → U1_gaa(X, Y, Z, average_in_aga(X, s(Y), Z))
average_in_aga(0, 0, 0) → average_out_aga(0, 0, 0)
average_in_aga(0, s(0), 0) → average_out_aga(0, s(0), 0)
average_in_aga(0, s(s(0)), s(0)) → average_out_aga(0, s(s(0)), s(0))
average_in_aga(s(X), Y, Z) → U1_aga(X, Y, Z, average_in_aga(X, s(Y), Z))
average_in_aga(X, s(s(s(Y))), s(Z)) → U2_aga(X, Y, Z, average_in_gaa(s(X), Y, Z))
average_in_gaa(X, s(s(s(Y))), s(Z)) → U2_gaa(X, Y, Z, average_in_gaa(s(X), Y, Z))
U2_gaa(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_gaa(X, s(s(s(Y))), s(Z))
U2_aga(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_aga(X, s(s(s(Y))), s(Z))
U1_aga(X, Y, Z, average_out_aga(X, s(Y), Z)) → average_out_aga(s(X), Y, Z)
U1_gaa(X, Y, Z, average_out_aga(X, s(Y), Z)) → average_out_gaa(s(X), Y, Z)
U2_agg(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_agg(X, s(s(s(Y))), s(Z))
U1_agg(X, Y, Z, average_out_agg(X, s(Y), Z)) → average_out_agg(s(X), Y, Z)
U1_gag(X, Y, Z, average_out_agg(X, s(Y), Z)) → average_out_gag(s(X), Y, Z)
average_in_gag(X, s(s(s(Y))), s(Z)) → U2_gag(X, Y, Z, average_in_gaa(s(X), Y, Z))
U2_gag(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_gag(X, s(s(s(Y))), s(Z))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PrologToPiTRSProof
AVERAGE_IN_GAG(s(X), Y, Z) → U1_GAG(X, Y, Z, average_in_agg(X, s(Y), Z))
AVERAGE_IN_GAG(s(X), Y, Z) → AVERAGE_IN_AGG(X, s(Y), Z)
AVERAGE_IN_AGG(s(X), Y, Z) → U1_AGG(X, Y, Z, average_in_agg(X, s(Y), Z))
AVERAGE_IN_AGG(s(X), Y, Z) → AVERAGE_IN_AGG(X, s(Y), Z)
AVERAGE_IN_AGG(X, s(s(s(Y))), s(Z)) → U2_AGG(X, Y, Z, average_in_gaa(s(X), Y, Z))
AVERAGE_IN_AGG(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GAA(s(X), Y, Z)
AVERAGE_IN_GAA(s(X), Y, Z) → U1_GAA(X, Y, Z, average_in_aga(X, s(Y), Z))
AVERAGE_IN_GAA(s(X), Y, Z) → AVERAGE_IN_AGA(X, s(Y), Z)
AVERAGE_IN_AGA(s(X), Y, Z) → U1_AGA(X, Y, Z, average_in_aga(X, s(Y), Z))
AVERAGE_IN_AGA(s(X), Y, Z) → AVERAGE_IN_AGA(X, s(Y), Z)
AVERAGE_IN_AGA(X, s(s(s(Y))), s(Z)) → U2_AGA(X, Y, Z, average_in_gaa(s(X), Y, Z))
AVERAGE_IN_AGA(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GAA(s(X), Y, Z)
AVERAGE_IN_GAA(X, s(s(s(Y))), s(Z)) → U2_GAA(X, Y, Z, average_in_gaa(s(X), Y, Z))
AVERAGE_IN_GAA(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GAA(s(X), Y, Z)
AVERAGE_IN_GAG(X, s(s(s(Y))), s(Z)) → U2_GAG(X, Y, Z, average_in_gaa(s(X), Y, Z))
AVERAGE_IN_GAG(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GAA(s(X), Y, Z)
average_in_gag(0, 0, 0) → average_out_gag(0, 0, 0)
average_in_gag(0, s(0), 0) → average_out_gag(0, s(0), 0)
average_in_gag(0, s(s(0)), s(0)) → average_out_gag(0, s(s(0)), s(0))
average_in_gag(s(X), Y, Z) → U1_gag(X, Y, Z, average_in_agg(X, s(Y), Z))
average_in_agg(0, 0, 0) → average_out_agg(0, 0, 0)
average_in_agg(0, s(0), 0) → average_out_agg(0, s(0), 0)
average_in_agg(0, s(s(0)), s(0)) → average_out_agg(0, s(s(0)), s(0))
average_in_agg(s(X), Y, Z) → U1_agg(X, Y, Z, average_in_agg(X, s(Y), Z))
average_in_agg(X, s(s(s(Y))), s(Z)) → U2_agg(X, Y, Z, average_in_gaa(s(X), Y, Z))
average_in_gaa(0, 0, 0) → average_out_gaa(0, 0, 0)
average_in_gaa(0, s(0), 0) → average_out_gaa(0, s(0), 0)
average_in_gaa(0, s(s(0)), s(0)) → average_out_gaa(0, s(s(0)), s(0))
average_in_gaa(s(X), Y, Z) → U1_gaa(X, Y, Z, average_in_aga(X, s(Y), Z))
average_in_aga(0, 0, 0) → average_out_aga(0, 0, 0)
average_in_aga(0, s(0), 0) → average_out_aga(0, s(0), 0)
average_in_aga(0, s(s(0)), s(0)) → average_out_aga(0, s(s(0)), s(0))
average_in_aga(s(X), Y, Z) → U1_aga(X, Y, Z, average_in_aga(X, s(Y), Z))
average_in_aga(X, s(s(s(Y))), s(Z)) → U2_aga(X, Y, Z, average_in_gaa(s(X), Y, Z))
average_in_gaa(X, s(s(s(Y))), s(Z)) → U2_gaa(X, Y, Z, average_in_gaa(s(X), Y, Z))
U2_gaa(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_gaa(X, s(s(s(Y))), s(Z))
U2_aga(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_aga(X, s(s(s(Y))), s(Z))
U1_aga(X, Y, Z, average_out_aga(X, s(Y), Z)) → average_out_aga(s(X), Y, Z)
U1_gaa(X, Y, Z, average_out_aga(X, s(Y), Z)) → average_out_gaa(s(X), Y, Z)
U2_agg(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_agg(X, s(s(s(Y))), s(Z))
U1_agg(X, Y, Z, average_out_agg(X, s(Y), Z)) → average_out_agg(s(X), Y, Z)
U1_gag(X, Y, Z, average_out_agg(X, s(Y), Z)) → average_out_gag(s(X), Y, Z)
average_in_gag(X, s(s(s(Y))), s(Z)) → U2_gag(X, Y, Z, average_in_gaa(s(X), Y, Z))
U2_gag(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_gag(X, s(s(s(Y))), s(Z))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PrologToPiTRSProof
AVERAGE_IN_GAA(s(X), Y, Z) → AVERAGE_IN_AGA(X, s(Y), Z)
AVERAGE_IN_AGA(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GAA(s(X), Y, Z)
AVERAGE_IN_AGA(s(X), Y, Z) → AVERAGE_IN_AGA(X, s(Y), Z)
AVERAGE_IN_GAA(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GAA(s(X), Y, Z)
average_in_gag(0, 0, 0) → average_out_gag(0, 0, 0)
average_in_gag(0, s(0), 0) → average_out_gag(0, s(0), 0)
average_in_gag(0, s(s(0)), s(0)) → average_out_gag(0, s(s(0)), s(0))
average_in_gag(s(X), Y, Z) → U1_gag(X, Y, Z, average_in_agg(X, s(Y), Z))
average_in_agg(0, 0, 0) → average_out_agg(0, 0, 0)
average_in_agg(0, s(0), 0) → average_out_agg(0, s(0), 0)
average_in_agg(0, s(s(0)), s(0)) → average_out_agg(0, s(s(0)), s(0))
average_in_agg(s(X), Y, Z) → U1_agg(X, Y, Z, average_in_agg(X, s(Y), Z))
average_in_agg(X, s(s(s(Y))), s(Z)) → U2_agg(X, Y, Z, average_in_gaa(s(X), Y, Z))
average_in_gaa(0, 0, 0) → average_out_gaa(0, 0, 0)
average_in_gaa(0, s(0), 0) → average_out_gaa(0, s(0), 0)
average_in_gaa(0, s(s(0)), s(0)) → average_out_gaa(0, s(s(0)), s(0))
average_in_gaa(s(X), Y, Z) → U1_gaa(X, Y, Z, average_in_aga(X, s(Y), Z))
average_in_aga(0, 0, 0) → average_out_aga(0, 0, 0)
average_in_aga(0, s(0), 0) → average_out_aga(0, s(0), 0)
average_in_aga(0, s(s(0)), s(0)) → average_out_aga(0, s(s(0)), s(0))
average_in_aga(s(X), Y, Z) → U1_aga(X, Y, Z, average_in_aga(X, s(Y), Z))
average_in_aga(X, s(s(s(Y))), s(Z)) → U2_aga(X, Y, Z, average_in_gaa(s(X), Y, Z))
average_in_gaa(X, s(s(s(Y))), s(Z)) → U2_gaa(X, Y, Z, average_in_gaa(s(X), Y, Z))
U2_gaa(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_gaa(X, s(s(s(Y))), s(Z))
U2_aga(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_aga(X, s(s(s(Y))), s(Z))
U1_aga(X, Y, Z, average_out_aga(X, s(Y), Z)) → average_out_aga(s(X), Y, Z)
U1_gaa(X, Y, Z, average_out_aga(X, s(Y), Z)) → average_out_gaa(s(X), Y, Z)
U2_agg(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_agg(X, s(s(s(Y))), s(Z))
U1_agg(X, Y, Z, average_out_agg(X, s(Y), Z)) → average_out_agg(s(X), Y, Z)
U1_gag(X, Y, Z, average_out_agg(X, s(Y), Z)) → average_out_gag(s(X), Y, Z)
average_in_gag(X, s(s(s(Y))), s(Z)) → U2_gag(X, Y, Z, average_in_gaa(s(X), Y, Z))
U2_gag(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_gag(X, s(s(s(Y))), s(Z))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PrologToPiTRSProof
AVERAGE_IN_GAA(s(X), Y, Z) → AVERAGE_IN_AGA(X, s(Y), Z)
AVERAGE_IN_AGA(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GAA(s(X), Y, Z)
AVERAGE_IN_AGA(s(X), Y, Z) → AVERAGE_IN_AGA(X, s(Y), Z)
AVERAGE_IN_GAA(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GAA(s(X), Y, Z)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Instantiation
↳ PiDP
↳ PrologToPiTRSProof
AVERAGE_IN_AGA(s) → AVERAGE_IN_GAA(s)
AVERAGE_IN_GAA(X) → AVERAGE_IN_GAA(s)
AVERAGE_IN_GAA(s) → AVERAGE_IN_AGA(s)
AVERAGE_IN_AGA(Y) → AVERAGE_IN_AGA(s)
AVERAGE_IN_AGA(s) → AVERAGE_IN_AGA(s)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ PiDP
↳ PrologToPiTRSProof
AVERAGE_IN_AGA(s) → AVERAGE_IN_AGA(s)
AVERAGE_IN_AGA(s) → AVERAGE_IN_GAA(s)
AVERAGE_IN_GAA(X) → AVERAGE_IN_GAA(s)
AVERAGE_IN_GAA(s) → AVERAGE_IN_AGA(s)
AVERAGE_IN_GAA(s) → AVERAGE_IN_GAA(s)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ NonTerminationProof
↳ PiDP
↳ PrologToPiTRSProof
AVERAGE_IN_AGA(s) → AVERAGE_IN_AGA(s)
AVERAGE_IN_GAA(s) → AVERAGE_IN_GAA(s)
AVERAGE_IN_AGA(s) → AVERAGE_IN_GAA(s)
AVERAGE_IN_GAA(s) → AVERAGE_IN_AGA(s)
AVERAGE_IN_AGA(s) → AVERAGE_IN_AGA(s)
AVERAGE_IN_GAA(s) → AVERAGE_IN_GAA(s)
AVERAGE_IN_AGA(s) → AVERAGE_IN_GAA(s)
AVERAGE_IN_GAA(s) → AVERAGE_IN_AGA(s)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PrologToPiTRSProof
AVERAGE_IN_AGG(s(X), Y, Z) → AVERAGE_IN_AGG(X, s(Y), Z)
average_in_gag(0, 0, 0) → average_out_gag(0, 0, 0)
average_in_gag(0, s(0), 0) → average_out_gag(0, s(0), 0)
average_in_gag(0, s(s(0)), s(0)) → average_out_gag(0, s(s(0)), s(0))
average_in_gag(s(X), Y, Z) → U1_gag(X, Y, Z, average_in_agg(X, s(Y), Z))
average_in_agg(0, 0, 0) → average_out_agg(0, 0, 0)
average_in_agg(0, s(0), 0) → average_out_agg(0, s(0), 0)
average_in_agg(0, s(s(0)), s(0)) → average_out_agg(0, s(s(0)), s(0))
average_in_agg(s(X), Y, Z) → U1_agg(X, Y, Z, average_in_agg(X, s(Y), Z))
average_in_agg(X, s(s(s(Y))), s(Z)) → U2_agg(X, Y, Z, average_in_gaa(s(X), Y, Z))
average_in_gaa(0, 0, 0) → average_out_gaa(0, 0, 0)
average_in_gaa(0, s(0), 0) → average_out_gaa(0, s(0), 0)
average_in_gaa(0, s(s(0)), s(0)) → average_out_gaa(0, s(s(0)), s(0))
average_in_gaa(s(X), Y, Z) → U1_gaa(X, Y, Z, average_in_aga(X, s(Y), Z))
average_in_aga(0, 0, 0) → average_out_aga(0, 0, 0)
average_in_aga(0, s(0), 0) → average_out_aga(0, s(0), 0)
average_in_aga(0, s(s(0)), s(0)) → average_out_aga(0, s(s(0)), s(0))
average_in_aga(s(X), Y, Z) → U1_aga(X, Y, Z, average_in_aga(X, s(Y), Z))
average_in_aga(X, s(s(s(Y))), s(Z)) → U2_aga(X, Y, Z, average_in_gaa(s(X), Y, Z))
average_in_gaa(X, s(s(s(Y))), s(Z)) → U2_gaa(X, Y, Z, average_in_gaa(s(X), Y, Z))
U2_gaa(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_gaa(X, s(s(s(Y))), s(Z))
U2_aga(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_aga(X, s(s(s(Y))), s(Z))
U1_aga(X, Y, Z, average_out_aga(X, s(Y), Z)) → average_out_aga(s(X), Y, Z)
U1_gaa(X, Y, Z, average_out_aga(X, s(Y), Z)) → average_out_gaa(s(X), Y, Z)
U2_agg(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_agg(X, s(s(s(Y))), s(Z))
U1_agg(X, Y, Z, average_out_agg(X, s(Y), Z)) → average_out_agg(s(X), Y, Z)
U1_gag(X, Y, Z, average_out_agg(X, s(Y), Z)) → average_out_gag(s(X), Y, Z)
average_in_gag(X, s(s(s(Y))), s(Z)) → U2_gag(X, Y, Z, average_in_gaa(s(X), Y, Z))
U2_gag(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_gag(X, s(s(s(Y))), s(Z))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PrologToPiTRSProof
AVERAGE_IN_AGG(s(X), Y, Z) → AVERAGE_IN_AGG(X, s(Y), Z)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Instantiation
↳ PrologToPiTRSProof
AVERAGE_IN_AGG(Y, Z) → AVERAGE_IN_AGG(s, Z)
AVERAGE_IN_AGG(s, z1) → AVERAGE_IN_AGG(s, z1)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Instantiation
↳ QDP
↳ ATransformationProof
↳ PrologToPiTRSProof
AVERAGE_IN_AGG(s, z1) → AVERAGE_IN_AGG(s, z1)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Instantiation
↳ QDP
↳ ATransformationProof
↳ QDP
↳ NonTerminationProof
↳ PrologToPiTRSProof
s(z1) → s(z1)
s(z1) → s(z1)
average_in_gag(0, 0, 0) → average_out_gag(0, 0, 0)
average_in_gag(0, s(0), 0) → average_out_gag(0, s(0), 0)
average_in_gag(0, s(s(0)), s(0)) → average_out_gag(0, s(s(0)), s(0))
average_in_gag(s(X), Y, Z) → U1_gag(X, Y, Z, average_in_agg(X, s(Y), Z))
average_in_agg(0, 0, 0) → average_out_agg(0, 0, 0)
average_in_agg(0, s(0), 0) → average_out_agg(0, s(0), 0)
average_in_agg(0, s(s(0)), s(0)) → average_out_agg(0, s(s(0)), s(0))
average_in_agg(s(X), Y, Z) → U1_agg(X, Y, Z, average_in_agg(X, s(Y), Z))
average_in_agg(X, s(s(s(Y))), s(Z)) → U2_agg(X, Y, Z, average_in_gaa(s(X), Y, Z))
average_in_gaa(0, 0, 0) → average_out_gaa(0, 0, 0)
average_in_gaa(0, s(0), 0) → average_out_gaa(0, s(0), 0)
average_in_gaa(0, s(s(0)), s(0)) → average_out_gaa(0, s(s(0)), s(0))
average_in_gaa(s(X), Y, Z) → U1_gaa(X, Y, Z, average_in_aga(X, s(Y), Z))
average_in_aga(0, 0, 0) → average_out_aga(0, 0, 0)
average_in_aga(0, s(0), 0) → average_out_aga(0, s(0), 0)
average_in_aga(0, s(s(0)), s(0)) → average_out_aga(0, s(s(0)), s(0))
average_in_aga(s(X), Y, Z) → U1_aga(X, Y, Z, average_in_aga(X, s(Y), Z))
average_in_aga(X, s(s(s(Y))), s(Z)) → U2_aga(X, Y, Z, average_in_gaa(s(X), Y, Z))
average_in_gaa(X, s(s(s(Y))), s(Z)) → U2_gaa(X, Y, Z, average_in_gaa(s(X), Y, Z))
U2_gaa(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_gaa(X, s(s(s(Y))), s(Z))
U2_aga(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_aga(X, s(s(s(Y))), s(Z))
U1_aga(X, Y, Z, average_out_aga(X, s(Y), Z)) → average_out_aga(s(X), Y, Z)
U1_gaa(X, Y, Z, average_out_aga(X, s(Y), Z)) → average_out_gaa(s(X), Y, Z)
U2_agg(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_agg(X, s(s(s(Y))), s(Z))
U1_agg(X, Y, Z, average_out_agg(X, s(Y), Z)) → average_out_agg(s(X), Y, Z)
U1_gag(X, Y, Z, average_out_agg(X, s(Y), Z)) → average_out_gag(s(X), Y, Z)
average_in_gag(X, s(s(s(Y))), s(Z)) → U2_gag(X, Y, Z, average_in_gaa(s(X), Y, Z))
U2_gag(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_gag(X, s(s(s(Y))), s(Z))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
average_in_gag(0, 0, 0) → average_out_gag(0, 0, 0)
average_in_gag(0, s(0), 0) → average_out_gag(0, s(0), 0)
average_in_gag(0, s(s(0)), s(0)) → average_out_gag(0, s(s(0)), s(0))
average_in_gag(s(X), Y, Z) → U1_gag(X, Y, Z, average_in_agg(X, s(Y), Z))
average_in_agg(0, 0, 0) → average_out_agg(0, 0, 0)
average_in_agg(0, s(0), 0) → average_out_agg(0, s(0), 0)
average_in_agg(0, s(s(0)), s(0)) → average_out_agg(0, s(s(0)), s(0))
average_in_agg(s(X), Y, Z) → U1_agg(X, Y, Z, average_in_agg(X, s(Y), Z))
average_in_agg(X, s(s(s(Y))), s(Z)) → U2_agg(X, Y, Z, average_in_gaa(s(X), Y, Z))
average_in_gaa(0, 0, 0) → average_out_gaa(0, 0, 0)
average_in_gaa(0, s(0), 0) → average_out_gaa(0, s(0), 0)
average_in_gaa(0, s(s(0)), s(0)) → average_out_gaa(0, s(s(0)), s(0))
average_in_gaa(s(X), Y, Z) → U1_gaa(X, Y, Z, average_in_aga(X, s(Y), Z))
average_in_aga(0, 0, 0) → average_out_aga(0, 0, 0)
average_in_aga(0, s(0), 0) → average_out_aga(0, s(0), 0)
average_in_aga(0, s(s(0)), s(0)) → average_out_aga(0, s(s(0)), s(0))
average_in_aga(s(X), Y, Z) → U1_aga(X, Y, Z, average_in_aga(X, s(Y), Z))
average_in_aga(X, s(s(s(Y))), s(Z)) → U2_aga(X, Y, Z, average_in_gaa(s(X), Y, Z))
average_in_gaa(X, s(s(s(Y))), s(Z)) → U2_gaa(X, Y, Z, average_in_gaa(s(X), Y, Z))
U2_gaa(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_gaa(X, s(s(s(Y))), s(Z))
U2_aga(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_aga(X, s(s(s(Y))), s(Z))
U1_aga(X, Y, Z, average_out_aga(X, s(Y), Z)) → average_out_aga(s(X), Y, Z)
U1_gaa(X, Y, Z, average_out_aga(X, s(Y), Z)) → average_out_gaa(s(X), Y, Z)
U2_agg(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_agg(X, s(s(s(Y))), s(Z))
U1_agg(X, Y, Z, average_out_agg(X, s(Y), Z)) → average_out_agg(s(X), Y, Z)
U1_gag(X, Y, Z, average_out_agg(X, s(Y), Z)) → average_out_gag(s(X), Y, Z)
average_in_gag(X, s(s(s(Y))), s(Z)) → U2_gag(X, Y, Z, average_in_gaa(s(X), Y, Z))
U2_gag(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_gag(X, s(s(s(Y))), s(Z))
AVERAGE_IN_GAG(s(X), Y, Z) → U1_GAG(X, Y, Z, average_in_agg(X, s(Y), Z))
AVERAGE_IN_GAG(s(X), Y, Z) → AVERAGE_IN_AGG(X, s(Y), Z)
AVERAGE_IN_AGG(s(X), Y, Z) → U1_AGG(X, Y, Z, average_in_agg(X, s(Y), Z))
AVERAGE_IN_AGG(s(X), Y, Z) → AVERAGE_IN_AGG(X, s(Y), Z)
AVERAGE_IN_AGG(X, s(s(s(Y))), s(Z)) → U2_AGG(X, Y, Z, average_in_gaa(s(X), Y, Z))
AVERAGE_IN_AGG(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GAA(s(X), Y, Z)
AVERAGE_IN_GAA(s(X), Y, Z) → U1_GAA(X, Y, Z, average_in_aga(X, s(Y), Z))
AVERAGE_IN_GAA(s(X), Y, Z) → AVERAGE_IN_AGA(X, s(Y), Z)
AVERAGE_IN_AGA(s(X), Y, Z) → U1_AGA(X, Y, Z, average_in_aga(X, s(Y), Z))
AVERAGE_IN_AGA(s(X), Y, Z) → AVERAGE_IN_AGA(X, s(Y), Z)
AVERAGE_IN_AGA(X, s(s(s(Y))), s(Z)) → U2_AGA(X, Y, Z, average_in_gaa(s(X), Y, Z))
AVERAGE_IN_AGA(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GAA(s(X), Y, Z)
AVERAGE_IN_GAA(X, s(s(s(Y))), s(Z)) → U2_GAA(X, Y, Z, average_in_gaa(s(X), Y, Z))
AVERAGE_IN_GAA(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GAA(s(X), Y, Z)
AVERAGE_IN_GAG(X, s(s(s(Y))), s(Z)) → U2_GAG(X, Y, Z, average_in_gaa(s(X), Y, Z))
AVERAGE_IN_GAG(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GAA(s(X), Y, Z)
average_in_gag(0, 0, 0) → average_out_gag(0, 0, 0)
average_in_gag(0, s(0), 0) → average_out_gag(0, s(0), 0)
average_in_gag(0, s(s(0)), s(0)) → average_out_gag(0, s(s(0)), s(0))
average_in_gag(s(X), Y, Z) → U1_gag(X, Y, Z, average_in_agg(X, s(Y), Z))
average_in_agg(0, 0, 0) → average_out_agg(0, 0, 0)
average_in_agg(0, s(0), 0) → average_out_agg(0, s(0), 0)
average_in_agg(0, s(s(0)), s(0)) → average_out_agg(0, s(s(0)), s(0))
average_in_agg(s(X), Y, Z) → U1_agg(X, Y, Z, average_in_agg(X, s(Y), Z))
average_in_agg(X, s(s(s(Y))), s(Z)) → U2_agg(X, Y, Z, average_in_gaa(s(X), Y, Z))
average_in_gaa(0, 0, 0) → average_out_gaa(0, 0, 0)
average_in_gaa(0, s(0), 0) → average_out_gaa(0, s(0), 0)
average_in_gaa(0, s(s(0)), s(0)) → average_out_gaa(0, s(s(0)), s(0))
average_in_gaa(s(X), Y, Z) → U1_gaa(X, Y, Z, average_in_aga(X, s(Y), Z))
average_in_aga(0, 0, 0) → average_out_aga(0, 0, 0)
average_in_aga(0, s(0), 0) → average_out_aga(0, s(0), 0)
average_in_aga(0, s(s(0)), s(0)) → average_out_aga(0, s(s(0)), s(0))
average_in_aga(s(X), Y, Z) → U1_aga(X, Y, Z, average_in_aga(X, s(Y), Z))
average_in_aga(X, s(s(s(Y))), s(Z)) → U2_aga(X, Y, Z, average_in_gaa(s(X), Y, Z))
average_in_gaa(X, s(s(s(Y))), s(Z)) → U2_gaa(X, Y, Z, average_in_gaa(s(X), Y, Z))
U2_gaa(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_gaa(X, s(s(s(Y))), s(Z))
U2_aga(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_aga(X, s(s(s(Y))), s(Z))
U1_aga(X, Y, Z, average_out_aga(X, s(Y), Z)) → average_out_aga(s(X), Y, Z)
U1_gaa(X, Y, Z, average_out_aga(X, s(Y), Z)) → average_out_gaa(s(X), Y, Z)
U2_agg(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_agg(X, s(s(s(Y))), s(Z))
U1_agg(X, Y, Z, average_out_agg(X, s(Y), Z)) → average_out_agg(s(X), Y, Z)
U1_gag(X, Y, Z, average_out_agg(X, s(Y), Z)) → average_out_gag(s(X), Y, Z)
average_in_gag(X, s(s(s(Y))), s(Z)) → U2_gag(X, Y, Z, average_in_gaa(s(X), Y, Z))
U2_gag(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_gag(X, s(s(s(Y))), s(Z))
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
AVERAGE_IN_GAG(s(X), Y, Z) → U1_GAG(X, Y, Z, average_in_agg(X, s(Y), Z))
AVERAGE_IN_GAG(s(X), Y, Z) → AVERAGE_IN_AGG(X, s(Y), Z)
AVERAGE_IN_AGG(s(X), Y, Z) → U1_AGG(X, Y, Z, average_in_agg(X, s(Y), Z))
AVERAGE_IN_AGG(s(X), Y, Z) → AVERAGE_IN_AGG(X, s(Y), Z)
AVERAGE_IN_AGG(X, s(s(s(Y))), s(Z)) → U2_AGG(X, Y, Z, average_in_gaa(s(X), Y, Z))
AVERAGE_IN_AGG(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GAA(s(X), Y, Z)
AVERAGE_IN_GAA(s(X), Y, Z) → U1_GAA(X, Y, Z, average_in_aga(X, s(Y), Z))
AVERAGE_IN_GAA(s(X), Y, Z) → AVERAGE_IN_AGA(X, s(Y), Z)
AVERAGE_IN_AGA(s(X), Y, Z) → U1_AGA(X, Y, Z, average_in_aga(X, s(Y), Z))
AVERAGE_IN_AGA(s(X), Y, Z) → AVERAGE_IN_AGA(X, s(Y), Z)
AVERAGE_IN_AGA(X, s(s(s(Y))), s(Z)) → U2_AGA(X, Y, Z, average_in_gaa(s(X), Y, Z))
AVERAGE_IN_AGA(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GAA(s(X), Y, Z)
AVERAGE_IN_GAA(X, s(s(s(Y))), s(Z)) → U2_GAA(X, Y, Z, average_in_gaa(s(X), Y, Z))
AVERAGE_IN_GAA(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GAA(s(X), Y, Z)
AVERAGE_IN_GAG(X, s(s(s(Y))), s(Z)) → U2_GAG(X, Y, Z, average_in_gaa(s(X), Y, Z))
AVERAGE_IN_GAG(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GAA(s(X), Y, Z)
average_in_gag(0, 0, 0) → average_out_gag(0, 0, 0)
average_in_gag(0, s(0), 0) → average_out_gag(0, s(0), 0)
average_in_gag(0, s(s(0)), s(0)) → average_out_gag(0, s(s(0)), s(0))
average_in_gag(s(X), Y, Z) → U1_gag(X, Y, Z, average_in_agg(X, s(Y), Z))
average_in_agg(0, 0, 0) → average_out_agg(0, 0, 0)
average_in_agg(0, s(0), 0) → average_out_agg(0, s(0), 0)
average_in_agg(0, s(s(0)), s(0)) → average_out_agg(0, s(s(0)), s(0))
average_in_agg(s(X), Y, Z) → U1_agg(X, Y, Z, average_in_agg(X, s(Y), Z))
average_in_agg(X, s(s(s(Y))), s(Z)) → U2_agg(X, Y, Z, average_in_gaa(s(X), Y, Z))
average_in_gaa(0, 0, 0) → average_out_gaa(0, 0, 0)
average_in_gaa(0, s(0), 0) → average_out_gaa(0, s(0), 0)
average_in_gaa(0, s(s(0)), s(0)) → average_out_gaa(0, s(s(0)), s(0))
average_in_gaa(s(X), Y, Z) → U1_gaa(X, Y, Z, average_in_aga(X, s(Y), Z))
average_in_aga(0, 0, 0) → average_out_aga(0, 0, 0)
average_in_aga(0, s(0), 0) → average_out_aga(0, s(0), 0)
average_in_aga(0, s(s(0)), s(0)) → average_out_aga(0, s(s(0)), s(0))
average_in_aga(s(X), Y, Z) → U1_aga(X, Y, Z, average_in_aga(X, s(Y), Z))
average_in_aga(X, s(s(s(Y))), s(Z)) → U2_aga(X, Y, Z, average_in_gaa(s(X), Y, Z))
average_in_gaa(X, s(s(s(Y))), s(Z)) → U2_gaa(X, Y, Z, average_in_gaa(s(X), Y, Z))
U2_gaa(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_gaa(X, s(s(s(Y))), s(Z))
U2_aga(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_aga(X, s(s(s(Y))), s(Z))
U1_aga(X, Y, Z, average_out_aga(X, s(Y), Z)) → average_out_aga(s(X), Y, Z)
U1_gaa(X, Y, Z, average_out_aga(X, s(Y), Z)) → average_out_gaa(s(X), Y, Z)
U2_agg(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_agg(X, s(s(s(Y))), s(Z))
U1_agg(X, Y, Z, average_out_agg(X, s(Y), Z)) → average_out_agg(s(X), Y, Z)
U1_gag(X, Y, Z, average_out_agg(X, s(Y), Z)) → average_out_gag(s(X), Y, Z)
average_in_gag(X, s(s(s(Y))), s(Z)) → U2_gag(X, Y, Z, average_in_gaa(s(X), Y, Z))
U2_gag(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_gag(X, s(s(s(Y))), s(Z))
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
AVERAGE_IN_GAA(s(X), Y, Z) → AVERAGE_IN_AGA(X, s(Y), Z)
AVERAGE_IN_AGA(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GAA(s(X), Y, Z)
AVERAGE_IN_AGA(s(X), Y, Z) → AVERAGE_IN_AGA(X, s(Y), Z)
AVERAGE_IN_GAA(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GAA(s(X), Y, Z)
average_in_gag(0, 0, 0) → average_out_gag(0, 0, 0)
average_in_gag(0, s(0), 0) → average_out_gag(0, s(0), 0)
average_in_gag(0, s(s(0)), s(0)) → average_out_gag(0, s(s(0)), s(0))
average_in_gag(s(X), Y, Z) → U1_gag(X, Y, Z, average_in_agg(X, s(Y), Z))
average_in_agg(0, 0, 0) → average_out_agg(0, 0, 0)
average_in_agg(0, s(0), 0) → average_out_agg(0, s(0), 0)
average_in_agg(0, s(s(0)), s(0)) → average_out_agg(0, s(s(0)), s(0))
average_in_agg(s(X), Y, Z) → U1_agg(X, Y, Z, average_in_agg(X, s(Y), Z))
average_in_agg(X, s(s(s(Y))), s(Z)) → U2_agg(X, Y, Z, average_in_gaa(s(X), Y, Z))
average_in_gaa(0, 0, 0) → average_out_gaa(0, 0, 0)
average_in_gaa(0, s(0), 0) → average_out_gaa(0, s(0), 0)
average_in_gaa(0, s(s(0)), s(0)) → average_out_gaa(0, s(s(0)), s(0))
average_in_gaa(s(X), Y, Z) → U1_gaa(X, Y, Z, average_in_aga(X, s(Y), Z))
average_in_aga(0, 0, 0) → average_out_aga(0, 0, 0)
average_in_aga(0, s(0), 0) → average_out_aga(0, s(0), 0)
average_in_aga(0, s(s(0)), s(0)) → average_out_aga(0, s(s(0)), s(0))
average_in_aga(s(X), Y, Z) → U1_aga(X, Y, Z, average_in_aga(X, s(Y), Z))
average_in_aga(X, s(s(s(Y))), s(Z)) → U2_aga(X, Y, Z, average_in_gaa(s(X), Y, Z))
average_in_gaa(X, s(s(s(Y))), s(Z)) → U2_gaa(X, Y, Z, average_in_gaa(s(X), Y, Z))
U2_gaa(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_gaa(X, s(s(s(Y))), s(Z))
U2_aga(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_aga(X, s(s(s(Y))), s(Z))
U1_aga(X, Y, Z, average_out_aga(X, s(Y), Z)) → average_out_aga(s(X), Y, Z)
U1_gaa(X, Y, Z, average_out_aga(X, s(Y), Z)) → average_out_gaa(s(X), Y, Z)
U2_agg(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_agg(X, s(s(s(Y))), s(Z))
U1_agg(X, Y, Z, average_out_agg(X, s(Y), Z)) → average_out_agg(s(X), Y, Z)
U1_gag(X, Y, Z, average_out_agg(X, s(Y), Z)) → average_out_gag(s(X), Y, Z)
average_in_gag(X, s(s(s(Y))), s(Z)) → U2_gag(X, Y, Z, average_in_gaa(s(X), Y, Z))
U2_gag(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_gag(X, s(s(s(Y))), s(Z))
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
AVERAGE_IN_GAA(s(X), Y, Z) → AVERAGE_IN_AGA(X, s(Y), Z)
AVERAGE_IN_AGA(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GAA(s(X), Y, Z)
AVERAGE_IN_AGA(s(X), Y, Z) → AVERAGE_IN_AGA(X, s(Y), Z)
AVERAGE_IN_GAA(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GAA(s(X), Y, Z)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Instantiation
↳ PiDP
AVERAGE_IN_AGA(s) → AVERAGE_IN_GAA(s)
AVERAGE_IN_GAA(X) → AVERAGE_IN_GAA(s)
AVERAGE_IN_GAA(s) → AVERAGE_IN_AGA(s)
AVERAGE_IN_AGA(Y) → AVERAGE_IN_AGA(s)
AVERAGE_IN_AGA(s) → AVERAGE_IN_AGA(s)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ PiDP
AVERAGE_IN_AGA(s) → AVERAGE_IN_AGA(s)
AVERAGE_IN_AGA(s) → AVERAGE_IN_GAA(s)
AVERAGE_IN_GAA(X) → AVERAGE_IN_GAA(s)
AVERAGE_IN_GAA(s) → AVERAGE_IN_AGA(s)
AVERAGE_IN_GAA(s) → AVERAGE_IN_GAA(s)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ NonTerminationProof
↳ PiDP
AVERAGE_IN_AGA(s) → AVERAGE_IN_AGA(s)
AVERAGE_IN_GAA(s) → AVERAGE_IN_GAA(s)
AVERAGE_IN_AGA(s) → AVERAGE_IN_GAA(s)
AVERAGE_IN_GAA(s) → AVERAGE_IN_AGA(s)
AVERAGE_IN_AGA(s) → AVERAGE_IN_AGA(s)
AVERAGE_IN_GAA(s) → AVERAGE_IN_GAA(s)
AVERAGE_IN_AGA(s) → AVERAGE_IN_GAA(s)
AVERAGE_IN_GAA(s) → AVERAGE_IN_AGA(s)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
AVERAGE_IN_AGG(s(X), Y, Z) → AVERAGE_IN_AGG(X, s(Y), Z)
average_in_gag(0, 0, 0) → average_out_gag(0, 0, 0)
average_in_gag(0, s(0), 0) → average_out_gag(0, s(0), 0)
average_in_gag(0, s(s(0)), s(0)) → average_out_gag(0, s(s(0)), s(0))
average_in_gag(s(X), Y, Z) → U1_gag(X, Y, Z, average_in_agg(X, s(Y), Z))
average_in_agg(0, 0, 0) → average_out_agg(0, 0, 0)
average_in_agg(0, s(0), 0) → average_out_agg(0, s(0), 0)
average_in_agg(0, s(s(0)), s(0)) → average_out_agg(0, s(s(0)), s(0))
average_in_agg(s(X), Y, Z) → U1_agg(X, Y, Z, average_in_agg(X, s(Y), Z))
average_in_agg(X, s(s(s(Y))), s(Z)) → U2_agg(X, Y, Z, average_in_gaa(s(X), Y, Z))
average_in_gaa(0, 0, 0) → average_out_gaa(0, 0, 0)
average_in_gaa(0, s(0), 0) → average_out_gaa(0, s(0), 0)
average_in_gaa(0, s(s(0)), s(0)) → average_out_gaa(0, s(s(0)), s(0))
average_in_gaa(s(X), Y, Z) → U1_gaa(X, Y, Z, average_in_aga(X, s(Y), Z))
average_in_aga(0, 0, 0) → average_out_aga(0, 0, 0)
average_in_aga(0, s(0), 0) → average_out_aga(0, s(0), 0)
average_in_aga(0, s(s(0)), s(0)) → average_out_aga(0, s(s(0)), s(0))
average_in_aga(s(X), Y, Z) → U1_aga(X, Y, Z, average_in_aga(X, s(Y), Z))
average_in_aga(X, s(s(s(Y))), s(Z)) → U2_aga(X, Y, Z, average_in_gaa(s(X), Y, Z))
average_in_gaa(X, s(s(s(Y))), s(Z)) → U2_gaa(X, Y, Z, average_in_gaa(s(X), Y, Z))
U2_gaa(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_gaa(X, s(s(s(Y))), s(Z))
U2_aga(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_aga(X, s(s(s(Y))), s(Z))
U1_aga(X, Y, Z, average_out_aga(X, s(Y), Z)) → average_out_aga(s(X), Y, Z)
U1_gaa(X, Y, Z, average_out_aga(X, s(Y), Z)) → average_out_gaa(s(X), Y, Z)
U2_agg(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_agg(X, s(s(s(Y))), s(Z))
U1_agg(X, Y, Z, average_out_agg(X, s(Y), Z)) → average_out_agg(s(X), Y, Z)
U1_gag(X, Y, Z, average_out_agg(X, s(Y), Z)) → average_out_gag(s(X), Y, Z)
average_in_gag(X, s(s(s(Y))), s(Z)) → U2_gag(X, Y, Z, average_in_gaa(s(X), Y, Z))
U2_gag(X, Y, Z, average_out_gaa(s(X), Y, Z)) → average_out_gag(X, s(s(s(Y))), s(Z))
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
AVERAGE_IN_AGG(s(X), Y, Z) → AVERAGE_IN_AGG(X, s(Y), Z)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Instantiation
AVERAGE_IN_AGG(Y, Z) → AVERAGE_IN_AGG(s, Z)
AVERAGE_IN_AGG(s, z1) → AVERAGE_IN_AGG(s, z1)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Instantiation
↳ QDP
↳ ATransformationProof
AVERAGE_IN_AGG(s, z1) → AVERAGE_IN_AGG(s, z1)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Instantiation
↳ QDP
↳ ATransformationProof
↳ QDP
↳ NonTerminationProof
s(z1) → s(z1)
s(z1) → s(z1)